Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:		from(X)	→ cons(X,from(s(X)))
2:		sel(0,cons(X,XS))	→ X
3:		sel(s(N),cons(X,XS))	→ sel(N,XS)
4:		minus(X,0)	→ 0
5:		minus(s(X),s(Y))	→ minus(X,Y)
6:		quot(0,s(Y))	→ 0
7:		quot(s(X),s(Y))	→ s(quot(minus(X,Y),s(Y)))
8:		zWquot(XS,nil)	→ nil
9:		zWquot(nil,XS)	→ nil
10:		zWquot(cons(X,XS),cons(Y,YS))	→ cons(quot(X,Y),zWquot(XS,YS))

There are 7 dependency pairs:


11:		FROM(X)	→ FROM(s(X))
12:		SEL(s(N),cons(X,XS))	→ SEL(N,XS)
13:		MINUS(s(X),s(Y))	→ MINUS(X,Y)
14:		QUOT(s(X),s(Y))	→ QUOT(minus(X,Y),s(Y))
15:		QUOT(s(X),s(Y))	→ MINUS(X,Y)
16:		ZWQUOT(cons(X,XS),cons(Y,YS))	→ QUOT(X,Y)
17:		ZWQUOT(cons(X,XS),cons(Y,YS))	→ ZWQUOT(XS,YS)

The approximated dependency graph contains 5 SCCs: {11}, {13}, {14}, {12} and {17}.

Consider the SCC {11}. There are no usable rules. The constraints could not be solved.

Consider the SCC {13}. There are no usable rules. By taking the AF π with π(MINUS) = 1 together with the lexicographic path order with empty precedence, rule 13 is strictly decreasing.

Consider the SCC {14}. The usable rules are {4,5}. By taking the AF π with π(QUOT) = 1 and π(minus) = π(s) = [ ] together with the lexicographic path order with precedence s ≻ minus ≻ 0, rule 5 is weakly decreasing and the rules in {4,14} are strictly decreasing.

Consider the SCC {12}. There are no usable rules. By taking the AF π with π(SEL) = 1 together with the lexicographic path order with empty precedence, rule 12 is strictly decreasing.

Consider the SCC {17}. There are no usable rules. By taking the AF π with π(ZWQUOT) = 1 and π(cons) = [2] together with the lexicographic path order with empty precedence, rule 17 is strictly decreasing.

Tyrolean Termination Tool (0.02 seconds) --- May 3, 2006